ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), i:Id, es:event_system{i:l}.
(x:Id. subtype_rel(es-vartype(es; i; x); fpf-cap(ds; id-deq; x; top)))
 (e:es-E(es). 
 (loc(e) = i)  subtype_rel(es-valtype(es; e); fpf-cap(da; Kind-deq; es-kind(es; e); top)))
 (e1,e2:es-E(es), L:(event-info(ds;da) List).
 (loc(e1) = i)
  (loc(e2) = i)
  ((L = []))
  iseg(event-info(ds;da); L; es-hist{i:l}(es;e1;e2))
  e[e1,e2].L = es-hist{i:l}(es;e1;e)) 

latex

Definitions

x:A. B(x), P  Q, A, iseg(T; l1; l2), es-locl(es; e; e'), t  T, prop{i:l}, x. t(x), x:A. B(x), P  Q, event-info(ds;da), P  Q, guard(T), e[e1,e2].P(e), A c B, T, True, wellfounded{i:l}(A; x,y.R(x;y)), x(s), es-hist{i:l}(es;e1;e2), decidable(P), False, P  Q, P  Q, map(f; as), Y

Lemmas

es-locl-wellfnd, false wf, es-hist wf, append wf, existse-between2 wf, es-loc wf, iseg wf, not wf, es-causl wf, es-E wf, es-valtype wf, fpf-cap wf, Kind-deq wf, es-kind wf, top wf, es-vartype wf, Id wf, id-deq wf, event system wf, fpf wf, Knd wf, decidable es-le, es-interval-is-nil, decidable es-locl, es-le-not-locl, iseg nil, assert of null, es-le-iff, es-pred wf, es-pred-locl, es-hist-last, es-locl transitivity1, iseg append single, decl-state wf, es-le-loc, es-loc-pred, es-info wf, es-le weakening, es-le wf, es-le weakening eq, squash wf, true wf